abstract class Tipo
case class TyInt() extends Tipo { override def toString = "int" }
case class TyBool() extends Tipo { override def toString = "bool" }
case class TyUnit() extends Tipo { override def toString = "unit" }
case class TyFun (t1: Tipo, t2: Tipo) extends Tipo { override def toString = "(" + t1 + " -> " + t2 + ")" }
case class TyRef (t: Tipo) extends Tipo { override def toString = t.toString + " ref" }
case class TyReg (eltos: List[(String,Tipo)]) extends Tipo { 
	override def toString = {
			eltos.foldLeft("{")((s, e) => s + e._1 + ": " + e._2 + ", ").dropRight(2) + "}"
	}

	def folder(s: String, e: (String, Tipo)): String = s + e._1 + ": " + e._2 + ", "
} 
case class TyTop() extends Tipo { override def toString = "top" }

abstract class Oper
case class Sum() extends Oper { override def toString = "+" }
case class Prod() extends Oper { override def toString = "*" }
case class Dif() extends Oper { override def toString = "/=" }
case class Eq() extends Oper { override def toString = "==" }
case class Geq() extends Oper { override def toString = ">=" }

abstract class Expr
case class N (n:Int) extends Expr { override def toString = n.toString }
case class B (b:Boolean) extends Expr { override def toString = b.toString }
case class BinOp (op: Oper, e1: Expr, e2: Expr) extends Expr { override def toString = e1.toString + op.toString + e2.toString } 
case class If (e1: Expr, e2: Expr, e3: Expr) extends Expr { override def toString = "if " + e1 + " then " + e2 + " else " + e3 + " fi" }
case class Asg (e1: Expr, e2: Expr) extends Expr { override def toString = e1.toString + " := " + e2 }
case class Deref (e: Expr) extends Expr { override def toString = "!" + e }
case class Ref (e: Expr) extends Expr { override def toString = "ref(" + e + ")" }
case class Skip() extends Expr { override def toString = "skip" }
case class Seq (e1: Expr, e2: Expr) extends Expr { override def toString = "(" + e1 + ";" + e2 + ")" }
case class W (e1: Expr, e2: Expr) extends Expr { override def toString = "while " + e1 + " do " + e2 + " done" }
case class Fun (x: String, t: Tipo, e: Expr) extends Expr { override def toString = "fn " + x + ": " + t + " => (" + e + ")" } 
case class App (e1 : Expr, e2: Expr) extends Expr { override def toString = "(" + e1 + " " + e2 + ")" }
case class Id (x: String) extends Expr { override def toString = x }
case class Let (x: String, t: Tipo, e1: Expr, e2: Expr) extends Expr { 
	override def toString = "let " + x + ": " + t + " = " + e1 + " in " + e2
} 
case class Reg (eltos: List[(String,Expr)]) extends Expr { 
	override def toString = eltos.foldLeft("{")((s, e) => s + e._1 + " = " + e._2 + ", ").dropRight(2) + "}"
}
case class Proj (lab: String, e: Expr) extends Expr { override def toString = "#" + lab + " " + e }

class L3 {
	var debug = false
	val debugSubtype = true
	val debugJoin = false
	val debugTypecheck = false
	
	var delta = List[(String, Expr)] ()
	
	type Gamma = List[(String, Tipo)]
	
	def typecheck(gamma: Gamma, e: Expr): Option[Tipo] = { 
			val t = e match {
			case N(_) => Some(TyInt())

			case B(_) => Some(TyBool())

			case BinOp(op, e1, e2) => op match {
			case Sum() => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			case (Some(TyInt()), Some(TyInt())) => Some(TyInt())
			case _ => None
			}

			case Prod() => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			case (Some(TyInt()), Some(TyInt())) => Some(TyInt())
			case _ => None
			}

			case Eq() => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			case (Some(TyInt()), Some(TyInt())) => Some(TyBool())
			case (Some(TyBool()), Some(TyBool())) => Some(TyBool())
			case _ => None
			}

			case Dif() => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			case (Some(TyInt()), Some(TyInt())) => Some(TyBool())
			case (Some(TyBool()), Some(TyBool())) => Some(TyBool())
			case _ => None
			}
			
			case Geq() => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			  case (Some(TyInt()), Some(TyInt())) => Some(TyBool())
			  case _ => None
			}
			}

			case Skip() => Some(TyUnit())

			case Seq(e1, e2) => typecheck(gamma, e1) match {
			case Some(TyUnit()) => typecheck(gamma, e2)
			case _ => None
			}

			case W(e1, e2) => (typecheck(gamma, e1), typecheck(gamma, e2)) match {
			case (Some(TyBool()), Some(TyUnit())) => Some(TyUnit())
			case _ => None
			}

			case Ref(e) => Some(TyRef(typecheck(gamma, e).get))

			case Deref(e) => typecheck(gamma, e) match {
			case Some(TyRef(t)) => Some(t)
			case _ => None
			}

			case Reg(el) => {
				var eltos = el map (te => (te._1, typecheck(gamma, te._2).get))
				Some(TyReg(eltos))
			}

			case Fun(x, t, e) => {
				val tf = typecheck((x, t) :: gamma, e)
				if (tf == None) None else Some(TyFun(t, tf.get))
			}

			case App(e1, e2) => typecheck(gamma, e1) match {
			case Some(TyFun(t1, t2)) => {
				val t3 = typecheck(gamma, e2)
				if (t3 == None) None else if (subtype(t3.get, t1)) Some(t2) else None
			}
			case _ => None
			}

			case Id(x) => gammaType(gamma, x)

			case Proj(lab, e) => typecheck(gamma, e) match {
			case Some(TyReg(el)) => {
				val elf = (el filter (e => e._1 == lab))
				if (elf.length == 0) None else Some(elf(0)._2)
			}
			case _ => None
			}

			case If(e1, e2, e3) => if (typecheck(gamma, e1) != Some(TyBool())) None else join(typecheck(gamma, e2), typecheck(gamma, e3))

			/*
			 * Por design, Asg não suporta subtipos sem cast explícito.
			 */
			case Asg(e1, e2) => {
			  val tLeft = typecheck(gamma, e1)
			  val tRight = typecheck(gamma, e2)
			  if (e2 != None) if (tLeft == Some(TyRef(tRight.get))) Some(TyUnit()) else None else None
			}

			case Let(x, t, e1, e2) => if (typecheck(gamma, e1) == Some(t)) typecheck((x, t) :: gamma, e2) else None 
			}
			if (debug && debugTypecheck) Console.println(gamma, e, t)
			t
	}

	def gammaType(gamma: Gamma, name: String): Option[Tipo] = {
			val list = gamma.filter(e => e._1 == name)
			if (list.length == 0) None else Some(list(0)._2)
	}

	/*
	 * Subtipos.
	 * - Para subtipagem de funções, a regra S-ARROW é seguida a risca: tipo esquerda da função sub é subtipo
	 *   do tipo esquerdo da função super, e o inverso nos valores da direita.
	 * - Para registros, a intersecção entre o subtipo e o supertipo deve ser igual ao supertipo, i.e. para cada tipo no
	 *   supertipo, se existe um subtipo deste tipo com o mesmo label, subt é subtipo de supert.
	 * - Todo tipo é subtipo de Top.
	 */
	def subtype(subt: Tipo, supert: Tipo): Boolean = {
			val isSubtype = (subt,supert) match {
			case (_, TyTop()) => true
			case (TyRef(refSub), TyRef(refSup)) => subtype(refSub, refSup)
			case (TyFun(s1, s2),TyFun(t1, t2)) => subtype(t1,s1) && subtype(s2,t2)
			case (TyReg(trsub),TyReg(trsup)) => 
			    val commons = trsup filter ((e1) => trsub exists ((e2) => (e1._1 equals e2._1) && subtype(e2._2, e1._2)))
			    if (debug && debugSubtype) Console println "Commons for " + trsup + " and " + trsub + " are " + commons
			    trsup == commons
			case _ => subt == supert
			}
			if (debug && debugSubtype) Console println (subt.toString + " is subtype of " + supert + " = " + isSubtype)
			isSubtype
	}
	
	/*
	 * Join busca pelo supertipo de t1 e t2.
	 * - Para funções (s1 -> s2, r1 -> r2), busca pelo supertipo de s1 e r1 e pelo supertipo de
	 *   s2 e r2.
	 * - Para registros, busca pela intersceção usando os tipo do supertipo.
	 */
	def join(t1: Option[Tipo], t2: Option[Tipo]): Option[Tipo] = {
			val newType = (t1, t2) match {
			case (Some(TyReg(eltos1)), Some(TyReg(eltos2))) => {
				val jeltos = eltos2 filter (t => eltos1 contains t)
				(if (jeltos.length == 0) Some(TyTop()) else Some(TyReg(jeltos)))
			}
			case (Some(TyFun(t1, t2)), Some(TyFun(s1, s2))) => {
				val j1 = join(Some(t1), Some(s1))
				val j2 = join(Some(t2), Some(s2))
				if (j1 == None || j2 == None) None else Some(TyFun(j1.get, j2.get))
			}
			case (Some(TyRef(t1)), Some(TyRef(t2))) => join(Some(t1), Some(t2))
			case (None, _) => None
			case (_, None) => None
			case _ => if (t1 == t2) t1 else Some(TyTop())
			}
			if (debug && debugJoin) Console println ("joined " + t1 + " and " + t2 + " to " + newType)
			newType
	}
}

object L3 {
	type Gamma = List[(String, Tipo)]

	                  def main(args: Array[String]) {
		val gamma = List[(String, Tipo)] ()

		// Caso de teste 1
		val TRa = TyReg(List (("a", TyInt())))
		val TRab = TyReg(List (("a", TyInt()), ("b", TyBool())))
		val f = Fun("x", TRa, Id("x"))
		val rab = Reg(List (("a", N(0)), ("b", B(true))))

		val internalLetBody = Proj("b", App(Id("f"), Id("rab")))
		val internalLet = Let("rab", TRab, rab, internalLetBody)

		val ct1 = Let("f", TyFun(TRa, TRa), f, internalLet)

		// Caso de teste 2
		val TRr = TyReg(List (("x", TyInt()), ("y", TyInt())))
		val Tr = TyRef(TRr)
		val proj = Proj("y", Deref(Id("r")))
		val fnr = Fun("r", Tr, proj)
		val regRef = Ref(Reg(List (("x", N(0)))))

		val ct2 = App(fnr, regRef)

		// Caso de teste 3
		val asg = Asg(Id("r"), Reg(List (("x", N(1)))))
		val internalSeq = Seq(asg, proj)
		val fnr2 = Fun("r", Tr, internalSeq)
		val reg2 = Reg(List (("x", N(0)), ("y", N(1))))
		val regRef2 = Ref(reg2)
		val ct3 = App(fnr2, regRef2)

		// Caso de teste 4
		val Tt = TyReg(List (("x", TyTop())))
		val xtProj = Proj("x", Id("t"))
		val fnt = Fun("t", Tt, xtProj)

		val ct4 = App(fnt, reg2)

		val exprs = List[(Expr, Option[Tipo])] (
				(ct1, None),
				(ct2, None),
				(ct3, None),
				(ct4, Some(TyTop()))
		)


		val interpreter = new L3()

		val failedTC = List ()

		var i = 0
		for (expr <- exprs) {
			i = i + 1
			if (failedTC contains i) interpreter.debug = true
			try {
				val t = interpreter.typecheck(gamma, expr._1)
				Console print (i.toString() + " " + (if (t == expr._2) "(    pass) " else "(Not pass) "))
				Console print(expr._1 + ": " + (if (t == None) "None" else t.get.toString))
				Console println (if (t != expr._2) " expected " + expr._2 else "") 
			} catch {
			case e: MatchError => Console println (e, expr)
			}
			if (failedTC contains i) interpreter.debug = false
		}
	}
}